(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 6))
(declare-fun a1 () (Array  (_ BitVec 5)  (_ BitVec 14)))
(declare-fun a2 () (Array  (_ BitVec 8)  (_ BitVec 8)))
(declare-fun a3 () (Array  (_ BitVec 9)  (_ BitVec 7)))
(assert (let ((e4(_ bv3 3)))
(let ((e5 (bvurem v0 v0)))
(let ((e6 (ite (bvsle e4 e4) (_ bv1 1) (_ bv0 1))))
(let ((e7 (store a3 ((_ sign_extend 3) e5) ((_ zero_extend 1) e5))))
(let ((e8 (select a2 ((_ sign_extend 7) e6))))
(let ((e9 (store a3 ((_ sign_extend 8) e6) ((_ sign_extend 6) e6))))
(let ((e10 (bvurem ((_ sign_extend 5) e6) e5)))
(let ((e11 (bvnor e8 ((_ sign_extend 2) v0))))
(let ((e12 (bvsub ((_ zero_extend 2) v0) e11)))
(let ((e13 (bvnor ((_ sign_extend 3) e4) e5)))
(let ((e14 (distinct v0 ((_ zero_extend 3) e4))))
(let ((e15 (bvsgt e12 e12)))
(let ((e16 (bvsgt e12 ((_ sign_extend 2) v0))))
(let ((e17 (bvslt ((_ sign_extend 2) e5) e11)))
(let ((e18 (bvuge e5 e10)))
(let ((e19 (distinct ((_ zero_extend 2) e10) e12)))
(let ((e20 (= e5 ((_ sign_extend 3) e4))))
(let ((e21 (bvuge ((_ zero_extend 2) e13) e11)))
(let ((e22 (= ((_ zero_extend 7) e6) e8)))
(let ((e23 (=> e20 e16)))
(let ((e24 (or e14 e23)))
(let ((e25 (xor e21 e17)))
(let ((e26 (=> e15 e24)))
(let ((e27 (or e19 e26)))
(let ((e28 (or e25 e27)))
(let ((e29 (and e28 e22)))
(let ((e30 (=> e29 e29)))
(let ((e31 (and e18 e30)))
(let ((e32 (and e31 (not (= v0 (_ bv0 6))))))
(let ((e33 (and e32 (not (= e5 (_ bv0 6))))))
e33
)))))))))))))))))))))))))))))))

(check-sat)
